보안 업체가 Miden zkVM 감사를 준비하며 AI 에이전트를 활용해 LSP 서버, 디컴파일러, 정적 분석 엔진, Lean 형식 모델을 6개월간 직접 구축한 사례를 소개한다. 이렇게 만든 도구들이 실제 보안 취약점(악성 프로버가 Falcon 서명을 위조해 자금을 탈취할 수 있는 미검증 입력 문제)을 발견했고, 95개의 기계 검증 정확성 증명을 확보했다. 코드 리뷰 외에도 감사 준비 단계부터 AI가 감사 품질과 깊이를 크게 높일 수 있음을 보여준다.
Bend는 C 수준의 속도로 네이티브 코드를 생성하고 CUDA 병렬화를 지원하며, Lean·Rocq 스타일의 증명 검사기를 통해 AI가 작성한 코드가 '법칙(LAWS.bend)'을 위반하지 않음을 수학적으로 보장하는 프로그래밍 언어입니다. AI 에이전트가 매 변경마다 1초 이내에 검증할 수 있어, 코드를 읽지 않고도 AI 생성 코드를 신뢰할 수 있게 하는 것이 핵심입니다.
이 글은 나비에-스토크스 증명 같은 화려한 성과에도 불구하고 LLM의 자율성이 과대평가됐다고 주장합니다. 저자는 순수수학이 엄밀한 명세가 이미 존재하는 최상의 시나리오일 뿐, 대부분의 지식 노동은 그렇지 않으며 보상 해킹(reward hacking) 문제를 막으려면 비싼 도메인 전문가의 엄밀한 명세 작성이 필요하다고 지적합니다.
OpenAI가 유체역학의 나비에-스토크스 방정식 관련 오랜 난제를 해결한 증명을 발표하며, 기존의 사람이 읽는 증명과 함께 기계 검증이 가능한 Lean 4 형식 증명도 함께 공개했습니다. 과거 학부 교과서 한 페이지를 형식화하는 데 약 40시간이 걸리던 것과 비교하면, OpenAI가 166페이지 논문의 증명을 17시간 만에 검증한 것은 비용을 4자리수(만 배) 수준으로 줄인 혁명적 변화입니다. 형식 검증은 수학뿐 아니라 보안 정책, 스마트 컨트랙트, 미션 크리티컬 알고리즘 검증에도 적용될 수 있습니다.
이 프로젝트는 3D 형상 연산(교집합) 알고리즘을 Lean 4로 구현하고 형식 검증(Formal verification)을 거친 사례입니다. 개발자는 복잡한 1,000줄 이상의 AI 생성 코드를 직접 검토할 필요 없이, 사람이 작성한 93줄의 핵심 명세와 Lean 컴파일러의 검증 결과만 신뢰하면 됩니다. 이를 통해 AI가 작성한 방대한 양의 코드와 증명 과정을 블랙박스로 처리하면서도 소프트웨어의 수학적 정확성을 완벽하게 보장받을 수 있음을 보여줍니다.
AI 스타트업 프라마나 랩스(Pramaana Labs)가 대형 언어 모델(LLM)의 오류와 환각을 잡기 위해 수학적 '형식 검증(Formal verification)'을 도입합니다. 이를 통해 법률, 세무, 신약 개발 등 오류가 치명적인 분야에서 기업들이 안전하게 AI를 활용할 수 있도록 돕고자 합니다.
천재 수학자 테렌스 타오는 AI가 수학 연구에 역사상 처음으로 '분업'을 도입할 수 있다고 주장합니다. 기존의 수학자들은 문제 설정부터 검증, 논문 작성까지 모든 것을 혼자 해야 했지만, 형식 검증 등 AI 기술의 도움으로 대규모 팀 간의 전문적 협업이 가능해진다는 것입니다. 다만, 인간의 통찰력과 엄격한 검증이 뒷받침될 때만 AI가 온전한 잠재력을 발휘할 수 있다고 강조하며 수학 연구의 패러다임 전환을 예고했습니다.
최신 LLM들이 동시성 및 분산 시스템 명세 언어인 TLA+를 사용해 시스템을 모델링하는 역량을 평가한 연구 결과입니다. 연구진이 개발한 자동화 벤치마크 'SysMoBench'에 따르면, 최신 LLM들은 문법이나 기본 실행 단계에서는 거의 완벽한 점수를 기록했지만, 실제 코드와 모델이 일치하는지 검증하는 단계(46%)와 핵심 속성을 만족하는지 확인하는 단계(41%)에서는 대폭 실패했습니다. 이는 현재 AI가 시스템 코드의 실제 구조를 추상화해 정확한 형식 모델을 작성하기보다는, 학습 데이터에 존재하는 교과서적인 예제를 단순히 암기하여 재생산하는 한계를 명확히 보여줍니다.